T:Type, X:MaInterface(T). ma-interface-inr(X)  MaInterface({x:Top + T| (isl(x))} ) 

latex

Definitions	Type, t  T, {x:A| B(x)} , Knd, b, Top, left + right, x:AB(x), x:A. B(x), State(ds), x:A  B(x), hasloc(k;i), x. t(x), a:A fp B(a), Id, (x  l), type List, MaInterface(T), False, P  Q, A, inr x , isl(x), Void, inl x , x.A(x), ma-interface-compose(g;X), ma-interface-inr(X)
Lemmas	not wf, ma-interface-compose wf, isl wf, false wf, l member wf, Id wf, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf